Code and Notes (Week 1 Tuesday)

import Data.Char

data Arith = Num Int | Var String
  | Plus Arith Arith | Times Arith Arith
  | Let String Arith Arith
  deriving Show


big_step :: Arith -> Int
big_step (Num i) = i
big_step (Plus e1 e2) = big_step e1 + big_step e2
big_step (Times e1 e2) = big_step e1 * big_step e2
big_step (Let nm e1 e2) =
  let v1 = big_step e1 in
  let e2_subst = subst nm (Num v1) e2 in
  big_step e2_subst
big_step (Var x) = error ("big_step: encountered var " ++ x)

-- substitute x for variables named nm in y
subst :: String -> Arith -> Arith -> Arith
subst nm x y = case y of
  Num _ -> y
  Plus a b -> Plus (subst nm x a) (subst nm x b)
  Times a b -> Times (subst nm x a) (subst nm x b)
  Let nm2 a b -> Let nm2 (subst nm x a)
    (if nm == nm2 then b else subst nm x b)
  Var nm2 -> if nm == nm2 then x else y

example_expr1 = Let "x"
    (Let "y" (Num 4) (Plus (Var "y") (Num 3))) (Var "x")
example_string1 = "let x = (let y = 4 in y + 3) in x"
example_string2 = "let x = (let y = 5 + 6 in y + y + 3) in x + 5 + (let z = 3 in z + 2)"


small_step :: Arith -> Maybe Arith
small_step (Num i) = Nothing
small_step (Plus (Num i) (Num j)) = Just (Num (i + j))
small_step (Plus (Num i) e2) = case small_step e2 of
    Just e2' -> Just (Plus (Num i) e2')
    Nothing -> Nothing
small_step (Plus e1 e2) = case small_step e1 of
    Just e1' -> Just (Plus e1' e2)
    Nothing -> Nothing
small_step (Times (Num i) (Num j)) = Just (Num (i + j))
small_step (Times (Num i) e2) = case small_step e2 of
    Just e2' -> Just (Times (Num i) e2')
    Nothing -> Nothing
small_step (Times e1 e2) = case small_step e1 of
    Just e1' -> Just (Times e1' e2)
    Nothing -> Nothing
small_step (Let nm (Num i) e2) = Just (subst nm (Num i) e2)
small_step (Let nm e1 e2) = case small_step e1 of
    Just e1' -> Just (Let nm e1' e2)
    Nothing -> Nothing
small_step (Var x) = error ("small_step: encountered var " ++ x)


small_steps (Num i) = [Num i]
small_steps e = case small_step e of
    Nothing -> error ("couldn't step: " ++ show e)
    Just e2 -> e : small_steps e2


data Token = LitT Int
  | LParenT | RParenT
  | EqualsT | PlusT | TimesT
  | LetT | InT | VarT String
  deriving Show

lexer :: String -> [Token]
lexer ('(' : cs) = LParenT : lexer cs
lexer (')' : cs) = RParenT : lexer cs
lexer ('+' : cs) = PlusT : lexer cs
lexer ('*' : cs) = TimesT : lexer cs
lexer ('=' : cs) = EqualsT : lexer cs
lexer [] = []
lexer (c : cs) = if isSpace c then lexer cs
  else if isDigit c
  then let (int_string, rest) = break (not . isDigit) (c : cs)
       in (LitT (read int_string) : lexer rest)
  else if isAlpha c
  then let (ident_str, rest) = break isSpace (c : cs)
       in (token_of_ident ident_str : lexer rest)
  else error ("couldn't lex this: " ++ show (c : cs))

token_of_ident s = if s == "let" then LetT else if s == "in" then InT
    else VarT s

parser_atom :: [Token] -> (Arith, [Token])
parser_atom (LitT i : ts) = (Num i, ts)
parser_atom (VarT nm : ts) = (Var nm, ts)
parser_atom (LParenT : ts) =
    let (expr, ts2) = parser_lexpr ts
    in case ts2 of
        RParenT : ts3 -> (expr, ts3)
        ts3 -> error ("expecting right parenthesis at: " ++ show ts3)
parser_atom ts = error ("not an atomic expression: " ++ show ts)

parser_pexpr :: [Token] -> (Arith, [Token])
parser_pexpr ts =
    let (expr, ts2) = parser_atom ts
    in case ts2 of
        TimesT : ts3 ->
            let (expr2, ts4) = parser_pexpr ts3
            in (Times expr expr2, ts4)
        _ -> (expr, ts2)

parser_sexpr :: [Token] -> (Arith, [Token])
parser_sexpr ts =
    let (expr, ts2) = parser_pexpr ts
    in case ts2 of
        PlusT : ts3 ->
            let (expr2, ts4) = parser_sexpr ts3
            in (Plus expr expr2, ts4)
        _ -> (expr, ts2)

parser_lexpr :: [Token] -> (Arith, [Token])
parser_lexpr (LetT : VarT nm : EqualsT : ts) =
    let (a, b) = error "matched a let _ = beginning" in
    let (expr, ts2) = parser_sexpr ts
    in case ts2 of
        InT : ts3 ->
            let (expr2, ts4) = parser_sexpr ts3
            in (Let nm expr expr2, ts4)
        ts3 -> error ("expecting 'in' token at: " ++ show ts3)
parser_lexpr ts = parser_sexpr ts

parser :: String -> Arith
parser s = case parser_lexpr (lexer s) of
  (expr, []) -> expr
  (expr, ts) -> error ("left-over tokens after parsing: " ++ show ts)

The goal is to prove the big-step and small-step
semantics are equivalent.


Let's start with the second case,

e →* Num n implies e ↓ n

The only sensible thing to do (I claim) is to induct on
the assumption e →* Num n, by rule induction using
the characterisation of reflexive transitive closure.

The induction ought (I claim) be used with a more general
assumption e →* e2, so that e and e2 can be instantiated
by the cases.

To do this, we prove the equivalent goal,
e →* e2 implies (!n. e2 = Num n implies e ↓ n),
using rule induction with P(e1, e2) ≡ (∀n. e2 = Num n implies e1 ↓ n).


The base case is the reflexive case, e →* e.

We must show P(e, e) ≡ (∀n. e = Num n implies e ↓ n),
which is exactly the Num case of the big-step rules.


The inductive case is associated with the step case
of the reflexive closure of the relation:

  e1 |-> e2   e2 |->* e3
  ----------------------
      e1 |->* e3

Our goal replaces the |->* judgements with P, that is,
we may assume e1 |-> e2 (the case assumption) and
P (e2, e3) (the inductive hypothesis).

We must show P(e1, e3) ≡ (!n. e3 = Num n implies e1 ↓ n).

So, we fix some n and assume e3 = Num n (call this the e3 premise).
We must show e1 ↓ n.

Our IH is P(e2, e2) ≡ (!n. e3 = Num n implies e2 ↓ n).
We pick the same n and combine this with the e3 premise to get e2 ↓ n.

Now we need to make use of our assumption e1 |-> e2. The small-step
relation is itself defined recursively for the various context cases
(which establish that we can small-step a compound expression by making
a small-step change at one of its inner expressions). The only sensible
thing to do (I claim) is to induct again.

Let us do this in the proof of a lemma that captures our current goal.
This lemma was shown on the slides:

   e |-> e'    e' ↓ n
   ------------------
         e ↓ n

This lemma makes intuitive sense. If we can adjust an expression via a
small-step, it should still evaluate to the same thing.

I claim that, for the induction to work out, we need to do it for all n,
since we won't know which n our inner expressions evaluate to.

So, let us prove this lemma:

e |-> e' implies (∀n. e' ↓ n implies e ↓ n)

This is again done by rule induction on the premise e |-> e', with
Q(e, e') ≡ (∀n. e' ↓ n implies e ↓ n)

This induction will involve 8 cases, one for each case of the small-step
relation. That's quite a few. Let's just look at one of them.

Here is the right-context rule for Plus:

         e2 |-> e2'
-----------------------------------
Plus (Num i) e2 |-> Plus (Num i) e2'

This rule lets us take a small step on the right hand side of a plus, assuming
the left hand side has already been evaluated down to a number.

The induction case associated with this rule has the IH
Q(e2, e2') ≡ (∀n. e2' ↓ n implies e2 ↓ n),
and the goal
Q(∀n. Plus (Num i) e2' ↓ n implies Plus (Num i) e2 ↓ n).

So, we fix n and assume our plus premise Plus (Num i) e2' ↓ n.

We now do a case-split on the derivation of this premise. Case splitting is
like induction, it requires a judgement and gives us goals for the different
cases by which this judgement might have been derived. The case-split
principle can be derived from the induction principle, roughly speaking, by
keeping the assumptions that the goal is of a particular shape and throwing the
IHs away.

Anyway, we have the plus premise Plus (Num i) e2' ↓ n. There is only one
big-step rule that can derive a big-step of a Plus.

This rule requires Num i ↓ v1 and e2' ↓ v2 (for some new v1 and v2) and shows
Plus (Num i) e2' ↓ (v1 + v2). So, we can assume that our n is v1 + v2 and that
we have Num i ↓ v1 and e2' ↓ v2. We could also case split on Num i ↓ v1, but
we don't need to for this proof.

We can now complete our derivation:

                          ------------ case-assum
                            e2' ↓ v2
  ----------- case-assum  ------------ IH
   Num i ↓ v1               e2 ↓ v2
  ------------------------------------ big-step Plus rule  ----------- case-assum
      Plus (Num i) e2 ↓ v1 + v2                            n = v1 + v2
      ---------------------------------------------------------------- subst of =
                 Plus (Num i) e2 ↓ n

That proves this case of our lemma proof.

The other "context cases" are all similar. Presume that e |-> e' and that e' wrapped
in some context evaluates to n, e.g. Let nm e' e2 ↓ n. Also assume the IH that
e' and e always big-step to the same n. Do cases on how e' in context evaluate big-step,
and specialise the problem to the relevant case, which will include a big-step
evaluation of e'. Apply the IH to get that e evaluates to the same thing alone, and
then use the rule for this case to give an evaluation of e in context. Finally,
observe that these evaluations in context gave the same value.

The "progress cases", e.g. the step Plus (Num i) (Num j) |-> Num (i + j) will
be provable by simply using the relevant big-step rule.

The slides claim the reverse case, assuming a big step evaluation, is easy. I
tried this in another framework, and I claim it is fiddly too. We will talk
about that briefly on Thursday.